The purpose of a program checking tool is to analyze a given computer program to determine whether or not it has certain desirable properties. Program checking tools, often called program checkers, are specific examples of verification systems that can also be used to analyze hardware components, formulae, algorithms, or, more generally, behavioral designs.
A good program checking tool has the property that the warnings it produces are informative and easy for a designer to understand. An informative warning message should, ideally, include a characterization of each possible defect (e.g., “array index out of bounds”, “timing constraint not satisfied”, “race condition”, “deadlock”, “failure to establish invariant”) and a source location in the computer program where the verification system tried, but failed, to show the absence of the defect (e.g., “line 218 of file ‘ABC.source’”). If a warning message is informative and easy to understand, the designer can more easily determine whether a warning is real or spurious, and what its cause is. The designer can then act accordingly, correcting the program at the source of the problem, or ignoring the warning, possibly annotating the program so that the warning will be suppressed next time the program checking tool is run. The cost of a programming error can be greatly reduced if it is detected early in the development process.
Dynamic, or run-time, checkers are a class of authoring tools that perform program checking functions and generate execution traces by executing or simulating the execution of the computer program in question. An example of such a tool is Eraser (S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson, “Eraser: A Dynamic Data Race Detector for Multithreaded Programming,” ACM Transactions on Computer Systems, 15(4):391–411, (1997)).
In general, the use of run-time checkers entails a number of disadvantages: there may be an overhead to their use, i.e., the program to be checked may make intensive use of expensive resources or may use resources not available to the run-time checker; some errors in the program may only manifest themselves under certain run-time conditions, such as certain values of the initial parameters, and thus may not be discovered by the run-time checker; and some errors may be non-reproducible.
By contrast, static checkers catch errors at compile time without executing the program and are valuable because they can be applied throughout the development cycle. A common example of a static checker is a type checker, which detects errors such as the application of a function to inappropriate argument values. An example of a static checker is PREfix (available from Intrinsa Corp., (1998)), Testbed Studio, (available from BiZZdesign BV, P.O. Box 321, 7500 AH Enschede, of The Netherlands; see also www.BiZZdesign.com/products/products.html). Another static checker is the Compaq Extended Static Checker for Java (“ESC/Java”), which checks for additional errors that are not caught by traditional type systems, such as dereferencing a null pointer, indexing an array outside its bounds, or accessing a shared variable without holding its protecting lock. ESC/Java uses an underlying automatic theorem prover to precisely reason about whether or not these kinds of errors can occur.
Static checkers generally rely on the programmer to supply annotations. The computer program may be annotated by a developer to indicate aspects that may not be apparent to the checker, or to impose restraints on how the program operates, or to describe program properties such as invariants. The annotations may permit the program checking tool to find defects using a local (modular) analysis, because the annotations provide a specification of other parts of the program. In modular checking, the static program checker analyses one program module at a time, where a module may be a function, subroutine or some suitable compartment of the program. During such a modular analysis, the program checking tool verifies that the supplied annotations are consistent with the program. The presence of the annotations guides the checking process, thus making the checking problem conceptually and computationally simpler.
For example, conventional type checkers follow this modular approach and rely on type annotations to guide the type checking process. Similarly, static race detection checkers, like rccjava (Flanagan, C., and Freund, S. N., “Type-based race detection for Java,” PLDI'00, ACM SIGPLAN Notices, 35(5):219–232, May 2000) rely on annotations describing the locking discipline. Additionally, extended static checkers like ESC/Modula-3 (Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B., “Extended Static Checking,” Research Report 159, Compaq Systems Research Center, December 1998) and ESC/Java (see www.research.compaq.com/SRC/esc/Esc.html) are modular checkers whose annotations include preconditions, postconditions, and object invariants.
The main costs in using a program checking tool, from the perspective of the programmer, comprise annotating the program, waiting for the tool to complete its analysis, and interpreting the tool's output. Often the dominant cost of using a program checking tool is annotating the program, especially for large legacy programs, because of the number of special constraints and conditions that need to be conveyed to the program checking tool via annotations.
Thus, a limitation of the modular checking approach is the burden on the programmer to supply annotations. Although programmers have grown accustomed to writing type annotations, they have been reluctant to provide additional annotations. This reluctance has been the major obstacle to the adoption of modular checkers like ESC/Java and rccjava. The burden of introducing annotations appears particularly pronounced when faced with the daunting task of applying such a checker to existing (unannotated) code bases. Preliminary experience with ESC/Java has indicated that a programmer can annotate an existing unannotated program at the rate of at most a few hundred lines per hour, though a lower rate is more usual if the programmer is unfamiliar with the code.
Some prior attempts at solving this problem have focused on modifying the program checking tool to eliminate the need for annotations altogether. An example of this approach is the abstract interpreter Syntox, for Pascal programs (Bourdoncle, F., “Abstract debugging of higher-order imperative languages.” Proceedings of the ACM SIGPLAN '93 Conference on Programming Language Design and Implementation, ACM SIGPLAN Notices, (June 1993), 28(6):46–55). Such an approach has a number of disadvantages. It may reduce the number of program properties that the tool can check, thereby reducing the overall usefulness of the tool. It may increase the number of warnings produced by the tool thereby causing a concomitant increase in the effort of interpreting the tool's output. And, without an annotation language, a programmer has no way to formally write down properties to be used and checked by the program checking tool.
Other prior attempts at solving this problem try to minimize, but not eliminate, the number of annotations required. An example of this approach is an ML-style type inference algorithm (where ML—“meta-language”—is a functional programming language, see Milner, R., “A theory of type polymorphism in programming,”Journal of Computer and System Sciences, (1978), 17(3):348–375; Damas, L. and Miner, R., “Principal type-schemes for functional programs,” Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, (POPL '82), 207–212, (January 1982)). This approach also has a number of disadvantages. For example, it may require a significant redesign of the program checking tool. The resulting tool may also be significantly more complicated, because it cannot rely on annotations to provide certain kinds of information.
Another prior attempt is a system for finding software defects called PREfix, cited hereinabove. It uses annotations, but these are not programmer-supplied. Instead, the annotations are inferred by PREfix and are stored in a database associated with the program being checked. This approach also has a number of disadvantages. Without a human-writeable annotation language, a programmer has no way to formally write down properties to be used and checked by the program checking tool. Without a human-readable annotation language, a programmer cannot inspect the annotations inferred by the tool. And, since PREfix both infers annotations and uses them, its design is different from, and is likely to be more complicated than, the design of a program checking tool that simply uses the annotations.
An approach not found in the prior art, and which is one of the foundations of the present invention, is to utilize the warnings produced by the program checking tool itself to infer annotations and to insert those annotations directly into the program. In this way, the program checking tool would function much as a black box in the sense that its internal workings are irrelevant for the purpose of the analysis. Such an approach could be repeated iteratively in such a way as to generate a modified computer program containing many new annotations at relatively little burden to the author but in such a way that the annotations would be intelligible.
A parser such as lex (see, for example, lex & yacc, 2nd Edition, by J. Levine, A. Mason & D. Brown, O'Reilly Publishing, (1992)) has not hitherto lent itself to such a scheme. Although parsers often suggest alterations to their input to correct lexical or syntactical errors and even act on these suggestions in the parser's internal representation of the input so the parser can continue to process the remainder of the input, such tools do not modify the program based on the suggestions and certainly do not iterate their analysis.
Similarly, LCLint is a tool that generates warnings about potential errors in programs (Evans, D., Guttag, J., Horning, J., and Tan, Y.-M., “LCLint: A tool for using specifications to check code,” in, ACM SIGSOFT Foundations in Software Engineering, pp. 87–96, Software Engineering Notes, 19(5), December 1994), but although it may output suggestions for how to fix these potential errors, it does not insert annotations into the program.
Additionally, an ML-style type inference algorithm, as described above, infers type annotations for an underlying type checker but neither uses the type checker iteratively nor as a black box, and does not write the inferred annotations into the computer program.
Accordingly, the present invention is designed to reduce the cost in annotating programs by using the program checking tool as a black box, thereby leveraging off the functionality of the program checking tool, rather than having to duplicate it.